perm filename KNOW.ART[F75,JMC]3 blob
sn#554808 filedate 1981-01-03 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .require "memo.pub[let,jmc]" source
C00035 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb AN AXIOMATIZATION OF KNOWLEDGE AND THE EXAMPLE OF THE WISE MAN PUZZLE
.cb John McCarthy
[Note: This memo was written in the Fall of 1975. As of September 1977,
the situation had changed in the following respects: (1) Chris
Goad did an axiomatization in which one could assert that a person
knows only what follows from a certain set of facts. This allows
proving that the first and second wise men don't know the colors of
their spots rather than assuming it. However, this axiomatization
seems unsatisfactory in various ways. (2) Morgan (1977) axiomatized
modal logic within first order logic (IEEE Computer Society
special issue on theorem proving). (3) The original McCarthy axiomatization
can be treated just as readily in first order logic as the axiomatization
involving possible worlds. (4) Sato's thesis has contributed much
to the semantics of knowledge systems. (5) The method of circumscription
has indicated that the way to circumscribe a
person's knowledge to a given set of facts should involve an axiom
schema.]
This memo reports results of a part of long continuing work
on the axiomatization of knowledge for the purposes of artificial
intelligence. Unfortunately, little of that work has been published
even informally, and this is a piece out of the middle, so to speak.
It is derived from the author's modal axiomatization of
knowledge, but is more directly based on a Kripke type semantics for
that modal system given by M. Sato of Kyoto Univerity. It owes
considerable to discussions with Professors Takasu and Igarashi and
Messrs. Hayashi and Sato of Kyoto University.
That axiomatization is distinguished from others in the
literature by the presence of an individual called FOOL, such that
anything FOOL knows, he knows that every one knows.
We work in the first order logic system associated with the
FOL proof-checker of Weyhrauch.
There are three sorts of individuals called persons,
propositions, and worlds. Each variable is confined to one of these
sorts, and the sort mechanism of FOL restricts the meaning of
quantification of a variable to the appropriate sort.
The first predicate is T(proposition,world) and means that
the proposition is true in the world. There is a function
K(person,proposition) which is a proposition asserting that person
knows the proposition serving as argument. The propositions of this
system are individuals with respect to the first order logic rather
than truth values or wffs. Therefore, we have to expicitly introduce
proposition-valued functions AND, OR, IMP, EQUIV, and NOT,
corresponding to the logical connectives ∧, ∨, ⊃, ≡, and ¬. Finally,
KW(s,p) is introduced as an abbreviation for K(s,p) ∨ K(s,NOT(p)) and
is read "s knows whether p".
Here is the axiom system in FOL notation. The declarations
establish the types of the variables and constants. The axioms are
essentially all definitions except for REFLEX which asserts that a
world is accessible from itself for any person.
DECLARE INDCONST FOOL ε PERSON;
DECLARE INDVAR S S1 S2 S3 S4 ε PERSON;
DECLARE INDVAR W W1 W2 W3 ε WORLD;
DECLARE INDVAR P P1 P2 P3 P4 Q Q1 Q2 Q3 Q4 R R1 R2 R3 R4 ε PROPOSITION;
DECLARE OPCONST K(PERSON,PROPOSITION) = PROPOSITION;
DECLARE OPCONST KW(PERSON,PROPOSITION) = PROPOSITION;
DECLARE OPCONST AND(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST OR(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST IMP(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST EQUIV(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST NOT(PROPOSITION) = PROPOSITION;
DECLARE PREDCONST T(PROPOSITION,WORLD);
DECLARE PREDCONST A(PERSON,WORLD,WORLD);
AXIOM REFLEX: ∀ S W.(A(S,W,W));;
AXIOM KNOW: ∀ S P W.(T(K(S,P),W) ≡ ∀W1.(A(S,W,W1) ⊃ T(P,W1)));;
AXIOM KW: ∀ S P W.(T(KW(S,P),W) ≡ T(K(S,P),W) ∨ T(K(S,NOT(P)),W));;
AXIOM FOOL: ∀ S P W.(T(K(FOOL,P),W) ⊃ T(K(FOOL,K(S,P)),W));;
AXIOM AND: ∀ W P Q.(T(AND(P,Q),W) ≡ T(P,W) ∧ T(Q,W));;
AXIOM OR: ∀ W P Q.(T(OR(P,Q),W) ≡ T(P,W) ∨ T(Q,W));;
AXIOM IMP: ∀ W P Q.(T(IMP(P,Q),W) ≡ T(P,W) ⊃ T(Q,W));;
AXIOM EQUIV: ∀ W P Q.(T(EQUIV(P,Q),W) ≡ (T(P,W) ≡ T(Q,W)));;
AXIOM NOT: ∀ W P.(T(NOT(P),W) ≡ ¬T(P,W));;
As an example of the use of these axioms, we do the following
puzzle of the three wise men.
"A certain king paints white spots on the foreheads of his
three wisemen who can see each other and are told that at least one
spot is white and the others black. He asks if any can tell the
color of his spot and after a while the wisest affirms that his spot
is white. The puzzle is to tell how he knows."
The solution is to say that the wisest reasons as follows:
"If my spot were black, the smarter of the remaining two would have
seen it and reasoned that if his spot were black, the slowest of us
would have seen two black spots and reasoned that his must be white."
In this form, the puzzle requires the wisest to reason about
how fast his colleagues think. We can get rid of this at the cost of
unfairness by having the king as each wise man in turn with the
answer being audible to the others. Another solution would have the
king not accept volunteered answers but repeat the question three
times, getting the correct answer from all three on the third
repetition.
Here are the axioms describing the puzzle:
DECLARE INDCONST WISE1 WISE2 WISE3 ε PERSON;
DECLARE INDCONST RW ε WORLD;
DECLARE INDCONST WHITE1 WHITE2 WHITE3 εPROPOSITION;
AXIOM WISEMAN:
T(WHITE1,RW)∧T(WHITE2,RW)∧T(WHITE3,RW),
T(K(FOOL,KW(WISE1,WHITE2)),RW),
T(K(FOOL,KW(WISE1,WHITE3)),RW),
T(K(FOOL,KW(WISE2,WHITE1)),RW),
T(K(FOOL,KW(WISE2,WHITE3)),RW),
T(K(FOOL,KW(WISE3,WHITE1)),RW),
T(K(FOOL,KW(WISE3,WHITE2)),RW),
T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW),
T(K(WISE3,K(WISE2,NOT(K(WISE1,WHITE1)))),RW),
T(K(WISE3,NOT(K(WISE2,WHITE2))),RW);
;
Next follows an annotated version of the FOL proof. Included
in the proof are the proofs of four lemmas that depend only on the
knowledge axioms and not on the specifics of the wise man puzzle.
Steps 1 thru 11 are a proof of the result of step 11, which
is a lemma to the effect that if S knows whether p and p is true,
then S knows p.
*****∀E KW S,P,W;
1 T(KW(S,P),W)≡(T(K(S,P),W)∨T(K(S,NOT(P)),W))
*****∀E REFLEX S,W;
2 A(S,W,W)
*****∀E KNOW S,NOT(P),W;
3 T(K(S,NOT(P)),W)≡∀W1.(A(S,W,W1)⊃T(NOT(P),W1))
*****∀E NOT W,P;
4 T(NOT(P),W)≡¬T(P,W)
*****ASSUME T(K(S,NOT(P)),W);
5 T(K(S,NOT(P)),W) (5)
***** 3,5;
6 ∀W1.(A(S,W,W1)⊃T(NOT(P),W1)) (5)
*****∀E ↑ W;
7 A(S,W,W)⊃T(NOT(P),W) (5)
*****⊃E 2,↑;
8 T(NOT(P),W) (5)
*****⊃I 5⊃↑;
9 T(K(S,NOT(P)),W)⊃T(NOT(P),W)
***** 1,4,9;
10 (T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W)
*****LABEL (KW1 . 11);
*****∀I ↑ S P W;
11 ∀S P W.((T(P,W)∧T(KW(S,P),W))⊃T(K(S,P),W))
Next comes a proof of the lemma on line 18 which asserts that
what S knows is true.
*****∀E KNOW S,P,W;
12 T(K(S,P),W)≡∀W1.(A(S,W,W1)⊃T(P,W1))
*****ASSUME T(K(S,P),W);
13 T(K(S,P),W) (13)
***** 12:13;
14 ∀W1.(A(S,W,W1)⊃T(P,W1)) (13)
*****∀E ↑ W;
15 A(S,W,W)⊃T(P,W) (13)
*****⊃E 2,↑;
16 T(P,W) (13)
*****⊃I 13⊃↑;
17 T(K(S,P),W)⊃T(P,W)
*****LABEL (KNOWTRUE . 18);
*****∀I ↑ S P W;
18 ∀S P W.(T(K(S,P),W)⊃T(P,W))
We begin the proof proper, and our first objective is the
assertions at step 23 and 24 that WISE3 knows WHITE1 and WHITE2, i.e.
he knows the spots of the other wisemen are white.
*****∀E ↑ FOOL,KW(WISE3,WHITE1),RW;
19 T(K(FOOL,KW(WISE3,WHITE1)),RW)⊃T(KW(WISE3,WHITE1),RW)
*****∀E ↑↑ FOOL,KW(WISE3,WHITE2),RW;
20 T(K(FOOL,KW(WISE3,WHITE2)),RW)⊃T(KW(WISE3,WHITE2),RW)
*****∀E 11 WISE3,WHITE1,RW;
21 (T(WHITE1,RW)∧T(KW(WISE3,WHITE1),RW))⊃T(K(WISE3,WHITE1),RW)
*****∀E 11 WISE3,WHITE2,RW;
22 (T(WHITE2,RW)∧T(KW(WISE3,WHITE2),RW))⊃T(K(WISE3,WHITE2),RW)
***** WISEMAN6,WISEMAN1,19,21;
23 T(K(WISE3,WHITE1),RW)
***** WISEMAN7,WISEMAN1,20,22;
24 T(K(WISE3,WHITE2),RW)
*****LABEL (ASS1 . 25);
Since our goal is an assertion that WISE3 knows WHITE3, which
must therefore be proved true in any world accessible to him, we
assume that W1 is an arbitrary such world. This assumption is not
discharged until step 131.
*****ASSUME A(WISE3,RW,W1);
25 A(WISE3,RW,W1) (25)
We now must prove the properties of W1. Many of them are
just properties of RW carried over as knowledge of FOOL or properties
that WISE3 knows in RW. The unindented lines 32, 33, and 40 and 41
are proved in this way.
*****∀E KNOW WISE3,WHITE1,RW;
26 T(K(WISE3,WHITE1),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE1,W1))
*****∀E KNOW WISE3,WHITE2,RW;
27 T(K(WISE3,WHITE2),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE2,W1))
***** 23,26;
28 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE1,W1))
***** 24,27;
29 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE2,W1))
*****∀E ↑↑ W1;
30 A(WISE3,RW,W1)⊃T(WHITE1,W1)
*****∀E ↑↑ W1;
31 A(WISE3,RW,W1)⊃T(WHITE2,W1)
*****⊃E 25,↑↑;
32 T(WHITE1,W1) (25)
*****⊃E 25,↑↑;
33 T(WHITE2,W1) (25)
*****∀E KNOW WISE3,K(WISE2,NOT(K(WISE1,WHITE1))),RW;
34 T(K(WISE3,K(WISE2,NOT(K(WISE1,WHITE1)))),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1))
*****∀E KNOW WISE3,NOT(K(WISE2,WHITE2)),RW;
35 T(K(WISE3,NOT(K(WISE2,WHITE2))),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1))
***** WISEMAN9,34;
36 ∀W1.(A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1))
***** WISEMAN10,35;
37 ∀W1.(A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1))
*****∀E ↑↑ W1;
38 A(WISE3,RW,W1)⊃T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)
*****∀E ↑↑ W1;
39 A(WISE3,RW,W1)⊃T(NOT(K(WISE2,WHITE2)),W1)
*****⊃E 25,↑↑;
40 T(K(WISE2,NOT(K(WISE1,WHITE1))),W1) (25)
*****⊃E 25,↑↑;
41 T(NOT(K(WISE2,WHITE2)),W1) (25)
Now it turns out that we need two more lemmas, one to the
effect that what FOOL knows, everyone knows he knows, and the other
to the effect what FOOL knows in any world, he knows in any world
accessible from it by any knower. It would have been more esthetic
to have proved these lemmas at the beginning, since, like the first
two, they don't involve the specifics of the wiseman puzzle. The
lemmas are lines 46 and 53.
*****∀E FOOL FOOL,P,W;
42 T(K(FOOL,P),W)⊃T(K(FOOL,K(FOOL,P)),W)
*****∀E FOOL S,K(FOOL,P),W;
43 T(K(FOOL,K(FOOL,P)),W)⊃T(K(FOOL,K(S,K(FOOL,P))),W)
*****∀E 18 FOOL,K(S,K(FOOL,P)),W;
44 T(K(FOOL,K(S,K(FOOL,P))),W)⊃T(K(S,K(FOOL,P)),W)
***** 42:44;
45 T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W)
*****LABEL (FOOL2 . 46);
*****∀I ↑ S W P;
46 ∀S W P.(T(K(FOOL,P),W)⊃T(K(S,K(FOOL,P)),W))
*****∀E KNOW S,K(FOOL,P),W;
47 T(K(S,K(FOOL,P)),W)≡∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1))
*****ASSUME T(K(FOOL,P),W);
48 T(K(FOOL,P),W) (48)
***** 45,47:48;
49 ∀W1.(A(S,W,W1)⊃T(K(FOOL,P),W1)) (48)
*****∀E ↑ W1;
50 A(S,W,W1)⊃T(K(FOOL,P),W1) (48)
*****⊃I ↑↑↑⊃↑;
51 T(K(FOOL,P),W)⊃(A(S,W,W1)⊃T(K(FOOL,P),W1))
***** 51;
52 (T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1)
*****LABEL (FOOLTRANS . 53);
*****∀I ↑ S P W W1;
53 ∀S P W W1.((T(K(FOOL,P),W)∧A(S,W,W1))⊃T(K(FOOL,P),W1))
With these lemmas, we transfer some of FOOL's knowledge to
W1, and the results are lines 59 thru 63.
*****∀E ↑ WISE3,KW(WISE1,WHITE2),RW,W1;
54 (T(K(FOOL,KW(WISE1,WHITE2)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE1,WHITE2)),W1)
*****∀E ↑↑ WISE3,KW(WISE1,WHITE3),RW,W1;
55 (T(K(FOOL,KW(WISE1,WHITE3)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE1,WHITE3)),W1)
*****∀E ↑↑↑ WISE3,KW(WISE2,WHITE1),RW,W1;
56 (T(K(FOOL,KW(WISE2,WHITE1)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE2,WHITE1)),W1)
*****∀E 53 WISE3,KW(WISE2,WHITE3),RW,W1;
57 (T(K(FOOL,KW(WISE2,WHITE3)),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,KW(WISE2,WHITE3)),W1)
*****∀E 53 WISE3,OR(WHITE1,OR(WHITE2,WHITE3)),RW,W1;
58 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),RW)∧A(WISE3,RW,W1))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)
***** WISEMAN2,25,54;
59 T(K(FOOL,KW(WISE1,WHITE2)),W1) (25)
***** WISEMAN3,25,55;
60 T(K(FOOL,KW(WISE1,WHITE3)),W1) (25)
***** WISEMAN4,25,56;
61 T(K(FOOL,KW(WISE2,WHITE1)),W1) (25)
***** WISEMAN5,25,57;
62 T(K(FOOL,KW(WISE2,WHITE3)),W1) (25)
***** WISEMAN8,25,58;
63 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1) (25)
In W1 we have that WISE2 doesn't know WHITE2, so we now find
a world in which WHITE2 is false accessible to WISE2 from W1. We
call it W2 and 69 and 70 give these results.
*****∀E KNOW WISE2,WHITE2,W1;
64 T(K(WISE2,WHITE2),W1)≡∀W.(A(WISE2,W1,W)⊃T(WHITE2,W))
*****∀E NOT W1,K(WISE2,WHITE2);
65 T(NOT(K(WISE2,WHITE2)),W1)≡¬T(K(WISE2,WHITE2),W1)
***** 41,64:65;
66 ¬∀W.(A(WISE2,W1,W)⊃T(WHITE2,W)) (25)
*****UNIFY↑;
67 ∃W.¬(A(WISE2,W1,W)⊃T(WHITE2,W)) (25)
*****∃E ↑ (W2);
68 ¬(A(WISE2,W1,W2)⊃T(WHITE2,W2)) (68)
***** 68;
69 A(WISE2,W1,W2) (68)
***** 68;
70 ¬T(WHITE2,W2) (68)
Now we have to establish the facts about W2, getting them
from the facts about W1 by the same methods as got the facts about W1
from RW. The additional facts we need are steps 76, 80, 86 and 91.
*****∀E 18 FOOL,KW(WISE2,WHITE1),W1;
71 T(K(FOOL,KW(WISE2,WHITE1)),W1)⊃T(KW(WISE2,WHITE1),W1)
*****∀E 11 WISE2,WHITE1,W1;
72 (T(WHITE1,W1)∧T(KW(WISE2,WHITE1),W1))⊃T(K(WISE2,WHITE1),W1)
*****∀E KNOW WISE2,WHITE1,W1;
73 T(K(WISE2,WHITE1),W1)≡∀W.(A(WISE2,W1,W)⊃T(WHITE1,W))
***** 32,61,71:73;
74 ∀W.(A(WISE2,W1,W)⊃T(WHITE1,W)) (25)
*****∀E ↑ W2;
75 A(WISE2,W1,W2)⊃T(WHITE1,W2) (25)
*****⊃E 69,↑;
76 T(WHITE1,W2) (25 68)
*****∀E KNOW WISE2,NOT(K(WISE1,WHITE1)),W1;
77 T(K(WISE2,NOT(K(WISE1,WHITE1))),W1)≡∀W.(A(WISE2,W1,W)⊃T(NOT(K(WISE1,WHITE1)),W))
***** 40,77;
78 ∀W.(A(WISE2,W1,W)⊃T(NOT(K(WISE1,WHITE1)),W)) (25)
*****∀E ↑ W2;
79 A(WISE2,W1,W2)⊃T(NOT(K(WISE1,WHITE1)),W2) (25)
*****⊃E 69,↑;
80 T(NOT(K(WISE1,WHITE1)),W2) (25 68)
*****∀E 53 WISE2,KW(WISE1,WHITE2),W1,W2;
81 (T(K(FOOL,KW(WISE1,WHITE2)),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,KW(WISE1,WHITE2)),W2)
*****∀E 53 WISE2,KW(WISE1,WHITE3),W1,W2;
82 (T(K(FOOL,KW(WISE1,WHITE3)),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,KW(WISE1,WHITE3)),W2)
*****∀E 53 WISE2,OR(WHITE1,OR(WHITE2,WHITE3)),W1,W2;
83 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W1)∧A(WISE2,W1,W2))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)
*****∀E 18 FOOL,KW(WISE1,WHITE2),W2;
84 T(K(FOOL,KW(WISE1,WHITE2)),W2)⊃T(KW(WISE1,WHITE2),W2)
*****∀E 18 FOOL,KW(WISE1,WHITE3),W2;
85 T(K(FOOL,KW(WISE1,WHITE3)),W2)⊃T(KW(WISE1,WHITE3),W2)
***** 59,68,81,84;
86 T(KW(WISE1,WHITE2),W2) (25 68)
***** 60,68,82,85;
87 T(KW(WISE1,WHITE3),W2) (25 68)
***** 63,68,83;
88 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2) (25 68)
*****∀E KW WISE1,WHITE2,W2;
89 T(KW(WISE1,WHITE2),W2)≡(T(K(WISE1,WHITE2),W2)∨T(K(WISE1,NOT(WHITE2)),W2))
*****∀E 18 WISE1,WHITE2,W2;
90 T(K(WISE1,WHITE2),W2)⊃T(WHITE2,W2)
***** 70,86,89:90;
91 T(K(WISE1,NOT(WHITE2)),W2) (25 68)
In W2, WISE1 doesn't know WHITE1, so there has to be an
accessible world from W2 in which WHITE1 is false, and establishing
this world W3 is accomplished at steps 97 and 98.
*****∀E KNOW WISE1,WHITE1,W2;
92 T(K(WISE1,WHITE1),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(WHITE1,W1))
*****∀E NOT W2,K(WISE1,WHITE1);
93 T(NOT(K(WISE1,WHITE1)),W2)≡¬T(K(WISE1,WHITE1),W2)
***** 80,92:93;
94 ¬∀W1.(A(WISE1,W2,W1)⊃T(WHITE1,W1)) (25 68)
*****UNIFY↑;
95 ∃W1.¬(A(WISE1,W2,W1)⊃T(WHITE1,W1)) (25 68)
*****∃E ↑ (W3);
96 ¬(A(WISE1,W2,W3)⊃T(WHITE1,W3)) (96)
***** 96;
97 A(WISE1,W2,W3) (96)
***** 96;
98 ¬T(WHITE1,W3) (96)
The only additional properties we have to transfer to W3 are
that WHITE2 is false and the disjunction WHITE1 ∨ WHITE2 ∨ WHITE3.
The first is established at step 103 and the second is essentially
transferred at step 106 though not isolated. These are used to
establishe WHITE3 in W3 at step 109.
*****∀E KNOW WISE1,NOT(WHITE2),W2;
99 T(K(WISE1,NOT(WHITE2)),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE2),W1))
***** 91,99;
100 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE2),W1)) (25 68)
*****∀E ↑ W3;
101 A(WISE1,W2,W3)⊃T(NOT(WHITE2),W3) (25 68)
*****∀E NOT W3,WHITE2;
102 T(NOT(WHITE2),W3)≡¬T(WHITE2,W3)
***** 97,101:102;
103 ¬T(WHITE2,W3) (25 68 96)
*****∀E 53 WISE1,OR(WHITE1,OR(WHITE2,WHITE3)),W2,W3;
104 (T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W2)∧A(WISE1,W2,W3))⊃T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)
***** 88,97,104;
105 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3) (25 68 96)
*****∀E 18 FOOL,OR(WHITE1,OR(WHITE2,WHITE3)),W3;
106 T(K(FOOL,OR(WHITE1,OR(WHITE2,WHITE3))),W3)⊃T(OR(WHITE1,OR(WHITE2,WHITE3)),W3)
*****∀E OR W3,WHITE1,OR(WHITE2,WHITE3);
107 T(OR(WHITE1,OR(WHITE2,WHITE3)),W3)≡(T(WHITE1,W3)∨T(OR(WHITE2,WHITE3),W3))
*****∀E OR W3,WHITE2,WHITE3;
108 T(OR(WHITE2,WHITE3),W3)≡(T(WHITE2,W3)∨T(WHITE3,W3))
***** 98,103,105:108;
109 T(WHITE3,W3) (25 68 96)
Now we have only to transfer WHITE3 back to W2 and finally to
W1 using the facts that WISE1 and WISE2 via whose accessibility
relations the transfers have to be made know whether WHITE3. These
results are obtained at steps 119 and 130 respectively.
*****∀E KW WISE1,WHITE3,W2;
110 T(KW(WISE1,WHITE3),W2)≡(T(K(WISE1,WHITE3),W2)∨T(K(WISE1,NOT(WHITE3)),W2))
*****∀E KNOW WISE1,NOT(WHITE3),W2;
111 T(K(WISE1,NOT(WHITE3)),W2)≡∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))
*****ASSUME ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1));
112 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1)) (112)
*****∀E ↑ W3;
113 A(WISE1,W2,W3)⊃T(NOT(WHITE3),W3) (112)
*****∀E NOT W3,WHITE3;
114 T(NOT(WHITE3),W3)≡¬T(WHITE3,W3)
***** 97,109,113:114;
115 FALSE (25 68 112)
*****⊃I 112⊃↑;
116 ∀W1.(A(WISE1,W2,W1)⊃T(NOT(WHITE3),W1))⊃FALSE (25 68)
***** 87,110:111,116;
117 T(K(WISE1,WHITE3),W2) (25 68)
*****∀E 18 WISE1,WHITE3,W2;
118 T(K(WISE1,WHITE3),W2)⊃T(WHITE3,W2)
*****⊃E ↑↑,↑;
119 T(WHITE3,W2) (25 68)
*****∀E 18 FOOL,KW(WISE2,WHITE3),W1;
120 T(K(FOOL,KW(WISE2,WHITE3)),W1)⊃T(KW(WISE2,WHITE3),W1)
*****∀E KW WISE2,WHITE3,W1;
121 T(KW(WISE2,WHITE3),W1)≡(T(K(WISE2,WHITE3),W1)∨T(K(WISE2,NOT(WHITE3)),W1))
*****∀E KNOW WISE2,NOT(WHITE3),W1;
122 T(K(WISE2,NOT(WHITE3)),W1)≡∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))
*****ASSUME ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W));
123 ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W)) (123)
*****∀E ↑ W2;
124 A(WISE2,W1,W2)⊃T(NOT(WHITE3),W2) (123)
*****∀E NOT W2,WHITE3;
125 T(NOT(WHITE3),W2)≡¬T(WHITE3,W2)
***** 69,119,124:125;
126 FALSE (25 123)
*****⊃I 123⊃↑;
127 ∀W.(A(WISE2,W1,W)⊃T(NOT(WHITE3),W))⊃FALSE (25)
***** 62,120:122,127;
128 T(K(WISE2,WHITE3),W1) (25)
*****∀E 18 WISE2,WHITE3,W1;
129 T(K(WISE2,WHITE3),W1)⊃T(WHITE3,W1)
*****⊃E ↑↑,↑;
130 T(WHITE3,W1) (25)
Since W1 is an arbitrary world accessible to WISE3 it follows
that WISE3 knows WHITE3 in RW, and four more steps suffice to
establish this.
*****⊃I 25⊃↑;
131 A(WISE3,RW,W1)⊃T(WHITE3,W1)
*****∀I ↑ W1;
132 ∀W1.(A(WISE3,RW,W1)⊃T(WHITE3,W1))
*****∀E KNOW WISE3,WHITE3,RW;
133 T(K(WISE3,WHITE3),RW)≡∀W1.(A(WISE3,RW,W1)⊃T(WHITE3,W1))
***** 132:133;
134 T(K(WISE3,WHITE3),RW)